g:IGroup, s:(|g|).
(s(e))
 (a:|g|. (s(a))  (s(~(a))))
 (a, b:|g|. (s(a))  (s(b))  (s(a * b)))
 EquivRel(|g|;x,y.x  y (mod s in g)) 

latex

Up	groups 1
Definitions	x:A. B(x), , P  Q, x f y, t  T, EquivRel(T;x,y.E(x;y)), a  b (mod s in g), P & Q, Refl(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Trans(T;x,y.E(x;y)), P  Q, P  Q, IGroup, IMonoid
Lemmas	grp car wf, grp op wf, grp inv wf, grp id wf, igrp wf, grp inverse, grp inv thru op, grp inv inv, mon assoc, grp inv assoc